(set-logic QF_BV)
(declare-fun x () (_ BitVec 3))
(declare-fun y () (_ BitVec 1))
(declare-fun z () (_ BitVec 21))
(assert 
  (let ((e6 ((_ zero_extend 15) x))) 
  (let ((e8 (bvsub (_ bv0 18) e6))) 
  (let ((e9 (bvadd ((_ sign_extend 20) y) z))) 
  (let ((e11 (bvule e9 ((_ sign_extend 3) e8)))) 
  (let ((e15 (bvslt z ((_ sign_extend 3) e8)))) 
  (let ((e61 (= e11 false))) 
  (let ((e63 e61)) 
  (let ((e64 e15)) 
  (let ((e65 (and e63 e64))) 
  (let ((e68 (= true e65))) 
  (let ((e69 (and e68 (not (= x (_ bv0 3)))))) 
  (let ((e70 e69)) e70)))))))))))))
(check-sat)
